<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    
<script type="text/javascript" src="js/moment.min.js"></script>
<script src="https://cdn.jsdelivr.net/npm/chart.js@2.9.3/dist/Chart.min.js"></script>

<script src="https://code.jquery.com/jquery-3.5.0.min.js" integrity="sha256-xNzN2a4ltkB44Mc/Jz3pT4iU1cmeR0FkXs4pru/JxaQ=" crossorigin="anonymous"></script>
<link href="https://unpkg.com/tabulator-tables@4.6.2/dist/css/tabulator.min.css" rel="stylesheet">
<script type="text/javascript" src="https://unpkg.com/tabulator-tables@4.6.2/dist/js/tabulator.min.js"></script>


	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Mathlib statistics</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  

  <div class="row mt-5">
    <div class="col-12">
      <h1>Mathlib statistics</h1>
    </div>
  </div>
  <div class="row mt-5">
    <h2>Declaration Counts</h2>
  </div>
  <div class="row mt-5">
    <div class="col-md-4">
      <h3>Definitions</h3>
      <h4>16404</h4>
    </div>
    <div class="col-md-4">
      <h3>Theorems</h3>
      <h4>33771</h4>
    </div>
    <div class="col-md-4">
      <h3>Meta declarations</h3>
      <h4>3813</h4>
    </div>
  </div>
 
  <div class="row mt-5">
    <h2>Code growth</h2>
  </div>
  <div class="row mt-5">
    <div class="col-md-6">
      <canvas id="files_by_date"></canvas>
    </div>

    <div class="col-md-6">
      <canvas id="lines_by_date"></canvas>
    </div>
  </div>

  <div class="row mt-5">
    <h2>Temporal distribution</h2>
  </div>
  <div class="row mt-5">
    <div class="col-md-6">
      <canvas id="by_year_month"></canvas>
    </div>

    <div class="col-md-6">
      <canvas id="by_year"></canvas>
    </div>
  </div>

  <div class="row mt-5">
    <h2>Authors</h2>

    <div class="col-12">
       <div id="authors_table"></div>
    </div>
  </div>
  <div class="row mt-5">

    <div class="col-md-12">
      <canvas id="lines_by_authors"></canvas>
    </div>

    <div class="col-md-12">
      <canvas id="commits_by_authors"></canvas>
    </div>
  </div>

  <div class="row mt-5">

  </div>

  </div>
</div>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
<script type="text/javascript" src="https://leanprover-community.github.io//mathlib_stats/gitstats.js"></script>

<script>

var color = Chart.helpers.color;
var blue = 'rgb(54, 162, 235)'

function makeBarChart(id, title, data) {
    var barChartData = {
        labels: data.labels,
        datasets: [{
            backgroundColor: color(blue).alpha(0.5).rgbString(),
            borderColor: blue,
            borderWidth: 1,
            data: data.data
        }]
    };

    var ctx = document.getElementById(id).getContext('2d');
    new Chart(ctx, {
        type: 'bar',
        data: barChartData,
        options: {
            responsive: true,
            legend: {
                display: false,
            },
            title: {
                display: true,
                text: title
            }
        }
    });
}

colors = ['#377eb8',
    '#ff0029',  '#66a61e', '#984ea3', '#00d2d5', '#ff7f00',
    '#af8d00', '#7f80cd', '#b3e900', '#c42e60', '#a65628', '#f781bf',
    '#8dd3c7', '#bebada', '#fb8072']

function makeLineChart(id, title, stamps, datas, show_title = true,
    show_legend = true) {
    var ctx = document.getElementById(id).getContext('2d');
    var datasets = []
    colidx = 0
    for (const [name, data] of Object.entries(datas)) {
        datasets.push(
           { label: name,
             fill: false,
             borderColor: colors[colidx],
             data: data,
             cubicInterpolationMode: 'monotone',
             pointRadius: 1,
           })
        colidx = colidx + 1
    };
    new Chart(ctx, {
        type: 'line',
        data: {
            labels: stamps,
            datasets : datasets
        },
        options: {
            title: {
                display: show_title,
                text: title
            },
            legend: {
                display: show_legend,
            },
            scales: {
                xAxes: [{
                    type: 'time',
                    time: {
                        unit: 'month',
                        parser: moment.unix,
                    },
                }]
            },
        },
    });
}
window.onload = function() {
    makeBarChart('by_year_month', 'Commits by month', by_year_month)
    makeBarChart('by_year', 'Commits by year', by_year)

    makeLineChart('lines_by_authors', 'Number of lines by author', stamps, lines_by_authors)
    makeLineChart('commits_by_authors', 'Number of commits by author', stamps, commits_by_authors)
    makeLineChart('files_by_date', 'Number of files', files_stamps,
        files_by_date, true, false)
    makeLineChart('lines_by_date', 'Number of lines', lines_stamps,
        lines_by_date, true, false)

    var table = new Tabulator("#authors_table", {
        data: authors, //set initial table data
        layout:"fitColumns",
        layoutColumnsOnNewData:true,
        responsiveLayout:true,
        columns: authors_cols,
        height: "600px",
    });
    table.redraw(true);

};


</script>

  </body>
</html>